\documentclass{llncs} 
\usepackage{graphicx}

\usepackage{listings}
% Define B sintaxe
\lstdefinelanguage{B}  {
keywords={MACHINE, REFINEMENT, REFINES, IMPLEMENTATION, SEES, IMPORTS, SETS, INCLUDES, EXTENDS, CONSTANTS, CONCRETE_CONSTANTS, CONCRETE_VARIABLES, PROPERTIES, DEFINITIONS, VARIABLES, ABSTRACT_VARIABLES, INITIALISATION, INVARIANT, VALUES, OPERATIONS, BEGIN, PRE, THEN, END, NAT, NAT1, BOOL, MAXINT, IF, ELSE, ELSIF, ANY, WHERE, CHOICE, OR, EITHER, SELECT, VAR, IN},
sensitive=true,% 
alsoletter={\$},% 
comment=[l]{\#},% 
string=[b]",% 
string=[b]'% 
}

% Set listing styles
\lstset{ %
%language=Pseudo,                % the language of the code
basicstyle=\footnotesize\ttfamily,            % the size of the fonts that are used for the code
extendedchars=true,
numbers=left,                   % where to put the line-numbers
numberstyle=\tiny,      % the size of the fonts that are used for the line-numbers 
%stepnumber=2,                   % the step between two line-numbers. If it's 1, each line will be numbered
%numbersep=5pt,                  % how far the line-numbers are from the code
%backgroundcolor=\color{white},  % choose the background color. You must add \usepackage{color}
%showspaces=false,               % show spaces adding particular underscores
%showstringspaces=false,         % underline spaces within strings
%showtabs=false,                 % show tabs within strings adding particular underscores
frame=b,   %trBL,                   % adds a frame around the code
stringstyle=\color{white}\ttfamily,
%linewidth=0.8\textwidth, % width of the line
tabsize=2,                      % sets default tabsize to 2 spaces
columns=fixed,
basewidth=.6em,
xleftmargin=20pt,
xrightmargin=5pt,
%captionpos=b,                   % sets the caption-position to bottom
breaklines=true,                % sets automatic line breaking
showspaces=false,           % Leerzeichen anzeigen ?
showtabs=false,             % Tabs anzeigen ?
%backgroundcolor=\color{lightgray},
%keywordstyle=\color{red},
showstringspaces=false
%breakatwhitespace=false,        % sets if automatic breaks should only happen at whitespace
%title=\lstname,                 % show the filename of files included with \lstinputlisting; also try caption instead of title
%escapeinside={\%*}{*)},         % if you want to add a comment within your code
%keywords={}            % if you want to add more keywords to the set
}

\sloppy
% The following is enclosed to allow easy detection of differences in
% ascii coding.
% Upper-case    A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
% Lower-case    a b c d e f g h i j k l m n o p q r s t u v w x y z
% Digits        0 1 2 3 4 5 6 7 8 9
% Exclamation   !           Double quote "          Hash (number) #
% Dollar        $           Percent      %          Ampersand     &
% Acute accent  '           Left paren   (          Right paren   )
% Asterisk      *           Plus         +          Comma         ,
% Minus         -           Point        .          Solidus       /
% Colon         :           Semicolon    ;          Less than     <
% Equals        =3D           Greater than >          Question mark ?
% At            @           Left bracket [          Backslash     \
% Right bracket ]           Circumflex   ^          Underscore    _
% Grave accent  `           Left brace   {          Vertical bar  |
% Right brace   }           Tilde        ~

% A couple of exemplary definitions:

\newcommand{\Nat}{{\mathbb N}}
\newcommand{\Real}{{\mathbb R}}

\begin{document}

\mainmatter

\title{Modeling the Java Card API in B \thanks{This work is partly supported by CAPES
 and CNPq grants 306033/2009-7, 560014/2010-4 and 573964/2008-4
 (National Institute of Science and Technology for Software Engineering---INES, \texttt{www.ines.org.br}).}}

\author{A. Martins Moreira\ \and S. de Oliveira Santos \and B. Gurgel Gomes \and D. D\'{e}harbe}
\institute{Federal University of Rio Grande do Norte (UFRN); Natal; Brazil}
%email{\{anamaria,david\}@dimap.ufrn.br, simone82@ppgsc.ufrn.br,bruno.gurgel@ifrn.edu.br}


\maketitle

\begin{abstract} 
  The B method development process starts from an abstract model of a
  set of services that are to be developed, and proceeds with formally
  verified refinements, which introduce implementation details. At a
  final refinement step these implementation details depend on the
  language for which code is to be generated. To rigorously develop
  Java Card Applications with the B method, then, it is necessary to
  model in B the constructs of Java Card, so that the gap between the
  B formally verified implementation model and the Java Card generated
  code be as narrow as possible. In the context of the BSmart project,
  we have developed the specification of the Java Card Application
  Programming Interface (Java Card API), to be used in the development
  of Java Card applications with B.
\end{abstract}

\section{Introduction}\label{intro}

In the context of the BSmart project, we are interested in the use of
B~\cite{BBook} to develop Java Card~\cite{chen:2000} applications.  Java Card is a
restricted and optimized version of Java which allows memory and
processor constrained devices, such as smart cards, to store and run
small applications.  Java Card applications have characteristics
(small size and need for security) which make them good candidates for
formal development with the B method. They also present some
regularity of structure that led our group to define a method and
implement a tool which specializes B for the development of such
applications, providing more focussed support for the developer than pure B
tools \cite{atelierB,proB}. They are the BSmart method and tool,
presented in \cite{BSmart08,Gomes10}.

Previous works have also dealt with B for Smart Cards,
\cite{Bert:2003,JBtools,tatibouet:lncs,requetBtoC}, but none has, to
our knowledge, specified Java Card in B so that the formal development
includes Java Card aspects. In the first versions of BSmart
\cite{Gomes10}, these aspects were included by the code generator. In 
contrast, with the JBTools~\cite{JBtools} approach, the generated code needed to be edited by
the developer to include these aspects. These works lacked then the ability to formally verify the Java Card
dependent aspects of the application. To change this, a B
specification of these aspects is needed, and this is the contribution
of this paper: the B specification of the Java Card API, with its
primitive types and all the classes of the 14 packages composing the
API. This specification can be used with the BSmart tool, 
independently, in any B tool, or even as a complement to the official
Java Card documentation \cite{oracle}.

In the following, we present some important aspects of the Java Card platform, in section \ref{sec:javacard}, and we introduce the B model of the Java Card API,  in section \ref{sec:api-spec}. We conclude with some notes on the use of the proposed model, in section \ref{sec:using-the-API}, and some conclusions and future work (in section \ref{sec:conc}).


\section{Smart Cards and Java Card}\label{sec:javacard}

A smart card application is distributed between on-card and off-card
components.  The server application on the card side (called applet)
provides the application services. The off-card client (called host
application) resides in a computer or electronic terminal. The information 
exchange between the host and card applications is
made through a  low level protocol, named
\emph{Application Protocol Data Unit} (APDU).  

The main component of the Java Card platform
is its runtime environment (JCRE), composed of a Java Card Virtual
Machine (JCVM), an Application Programming Interface (API), and, usually, system and
industry-specific classes~\cite{chen:2000}. The JCRE acts as a small
operating system, being responsible for the control of the application
lifetime, security and resource management.

The Java Card API is the part of the Java Card platform that a developer of any Java Card application must use. It defines the constituents of an applet, provides the means to deal with the APDU protocol and to communicate data and commands between the host application and the card. It also defines some basic security services such as encryption.

In a Java Card application, the applet is the part which defines the card provided services. 
An applet inherits the \emph{javacard.framewok.Applet} class of the Java Card API and is
implemented upon the Java Card subset of Java to provide these services.  During the applet
conversion for card installation, a verification phase is performed to
check conformance of the classes to Java Card restrictions.

\section{B specification of the Java Card API}\label{sec:api-spec}

\paragraph{Motivation}
Among the different components of the Java Card platform, the Java
Card API is the one without which no refinement into Java Card code
could be done.  Suppose, for instance, that we had the B abstract
machine of Listing~\ref{lis:buscard}, which models a bus card with a
variable that keeps track of the current credit the user has
(\texttt{balance}) and an operation to add credits to this balance
(\texttt{add}). This simple example provides enough evidence of the
importance of having a B model of the Java Card API.  B tools can
directly generate code for it in C, for instance, because it is a
deterministic specification and all data in it is implementable in C.
The resulting code would be very similar to the original B machine.

\lstset{language=B, caption={B machine Buscard},label=lis:buscard}
\begin{lstlisting}
MACHINE	Buscard
CONSTANTS	MAX_BALANCE
PROPERTIES	MAX_BALANCE : INTEGER & MAX_BALANCE  = 100
VARIABLES	balance
INVARIANT	balance : INTEGER & balance <= MAX_BALANCE 
INITIALISATION balance := 0
OPERATIONS
	add(credit) =
	PRE 	credit : INTEGER &  
		credit > 0  & credit <= MAX_BALANCE & 
		balance + credit <= MAX_BALANCE 
	THEN balance := balance + credit
	END
END
\end{lstlisting}

However, Java Card code corresponding to the operation \texttt{add} of
this B specification would look like the one presented in
Listing~\ref{lis:addjavacard}. In a rigorous development process, we do
not want the code generator to carry out all these non-verified
transformations in the code. So, we need to be able to refine the
original B machine into something such as the B refinement of
Listing~\ref{lis:addimplementation}. Then, code generation would be
straightforward (as it should be).

\lstset{language=Java, caption={Method add in applet Java Card},label=lis:addjavacard}
\begin{lstlisting}
public void add (APDU apdu) { 
	byte[] bf;  byte cr; byte apdu_state; short res;			
	bf = apdu.getBuffer();
	apdu_state = apdu.getCurrentState();
	if (apdu_state == STATE_INITIAL) { 
			res = apdu.setIncomingAndReceive();} 
	else if ( ISO7816.OFFSET_CDATA >= 0 && bf != null &&
		(short) (ISO7816.OFFSET_CDATA + 2) <= bf.length) {
			cr = Util.getShort (bf, ISO7816.OFFSET_CDATA);
		if (!(cr <= MAX_BALANCE)) {	
			ISOException.throwIt(EX_CREDIT_EXCEEDED);
		} else if (!((short) (balance + cr) <= MAX_BALANCE)) {
			ISOException.throwIt(EX_BALANCE_EXCEEDED);
		} else if (! (cr > 0)) { 
			ISOException.throwIt(EX_NEGATIVE_CREDIT);
		} else {balance = (short) (balance + cr);}}}
\end{lstlisting}

\lstset{language=B, caption={B implementation},label=lis:addimplementation}
\begin{lstlisting}
add (apdu) = 
VAR 	bf, cr, apdu_state, res
IN
	bf  <-- apdu.getBuffer;		
    	apdu_state  <-- apdu.getCurrentState;
	IF (apdu_state = STATE_INITIAL) 
	THEN res <-- apdu.setIncomingAndReceive                
	ELSIF (OFFSET_CDATA >= 0 &
		sum_short(OFFSET_CDATA, 2) <= size(bf) & 
		bf /= [])
	THEN 
		cr  <-- Util.getShort(bf, OFFSET_CDATA);
		IF not (cr <= MAX_BALANCE)
		THEN ISOException.throwIt(EX_CREDIT_EXCEEDED)
		ELSIF not (sum_short (balance, cr) <= MAX_BALANCE)
		THEN ISOException.throwIt(EX_BALANCE_EXCEEDED)
		ELSIF not (cr > 0)
		THEN ISOException.throwIt(EX_NEGATIVE_CREDIT) 
		ELSE  balance := sum_short(balance, cr)
		END
	END
END
\end{lstlisting}

We can identify two main kinds of transformation that have to be
carried out in order to obtain the code of operation \texttt{add} in
figs.~\ref{lis:addjavacard} and~\ref{lis:addimplementation} from the
abstract specification in Listing~\ref{lis:buscard}:

\begin{enumerate}
\item the transition into a defensive style of programming by the
  inclusion of explicit tests to check that the input conditions (pre
  conditions in the B specification) are satisfied before executing
  the corresponding action;

\item the inclusion of Java Card specific aspects, such as changing
  the signature of \texttt{add} so that data is transmitted via the
  APDU protocol and the APDU buffer is manipulated by methods offered
  the Java Card API.

\end{enumerate}

The transition to a defensive style of programming is part of the
BSmart method and tool, which generates a B refinement of the original
specification where pre-conditions are transformed into conditionals
(IF-THEN-ELSE-END constructs), with the indication of the need to
throw the corresponding exception when the specified conditions are
not met by input data and states.  The resulting B model can then be
formally verified as usual in the B method.

The change of interface is also taken care of by the BSmart method, so
that the development can be done without extending the B
method, as presented in~\cite{Gomes10}.

But all of these transformations rely on the need to reference Java
Card API types, classes and methods on the B level.  This is then the
reason why the Java Card API needed to be the first Java Card
component to be modeled in B. This is a common choice, as we can see
in previous work on the formalization of Java Card in JML
\cite{pollBerg01} and OCL \cite{Larsson:2004}.

\paragraph{The model}
The Java Card API, in its version 2.2.2\footnote{Java Card 2.2.2,
  although not the most recent version of the Java Card platform, is
  still widely used, and can easily be extended to Java Card 3 Classic
  Edition, a backward compatible evolution of version 2.2.2.,
  including some bug fixes, clarifications against the Java Card
  v2.2.2 specifications and new security algorithms (Java Card 3
  Platform Release Notes, available at
  http://www.oracle.com/technetwork/java/javame/javacard/download/overview/index.html).}, is composed of 14
packages, containing 93 classes and interfaces. Their interfaces have all been modeled in B,
and the resulting models are available at the KitSmart project
page\footnote{https://code.google.com/p/kitsmart/}.  Differently from
JML and OCL, though, B is not object oriented, and some modeling
solutions had to be found to cope with this lack of resources.  We
present in the following the main characteristics and some
restrictions of our models:
%
%\begin{table}[h]
%\begin{center}
%\caption{Packages of the Java Card API (2.2.2) and the number of classes in each package.}
%\begin{tabular}{|l|c||l|c|}
% \hline
% 
%\textbf{\small{Package}} & \textbf{\small{classes}} & \textbf{\small{Package}} & \textbf{\small{classes}}\\ \hline \hline
%\small{java.io} & \small{1} & \small{javacardx.biometry} & \small{5} \\ \hline
%\small{java.lang} & \small{12} & \small{javacardx.crypto }& \small{2} \\ \hline
%\small{java.rmi} & \small{2} & \small{javacardx.external} & \small{3} \\ \hline
%\small{javacard.framework} & \small{19} & \small{javacardx.framework.math} & \small{3} \\ \hline
%\small{javacard.framework.service} & \small{8} & \small{javacardx.framework.tlv} & \small{7} \\ \hline
%\small{javacard.security} & \small{27} & \small{javacardx.framework.util} & \small{2} \\ \hline
%\small{javacardx.apdu} & \small{1} & \small{javacardx.framework.util.intx} & \small{1} \\
%
% \hline
%\end{tabular}
%\label{tab:packages}
%\end{center}
%\end{table}

\begin{itemize}

\item Only the abstract models corresponding to each class or
  interface have been developed. Two reasons led to this choice: (1)
  code is not to be generated from the specification of the API, as we
  are only creating a model fo existing implementations; and
  (2) in B, only the abstract machines are seen by modules that build
  upon others, through the SEES, USES, IMPORTS, INCLUDES and EXTENDS
  clauses.

\item Conditions on method inputs which may lead to exception raising
  in the Java Card platform specification are coded into
  pre-conditions in B.
  
\item Method outputs are modeled in B as taking any value of the
  correct type, or, when possible in the current abstraction level,
  any value of a more restricted set of specified return values.
  
\item In the current version of the specification, states are not
  modeled.  The B machines corresponding to Java Card classes or
  interfaces are stateless.
  
\item Each machine corresponding to a Java Card class defines an
  abstract set with the same name (distinction on character cases,
  only). For instance, the machine Throwable declares the abstract set
  THROWABLE. This set can then be used to reference the type
  corresponding to the class.

\item The hierarchy of the Java Card API objects is partially modeled
  by abstract set inclusion. For instance, the class Throwable extends
  the class Object, in Java Card. In our model, we  have that the
  machine Throwable SEES the machine Object, and to constrain that all throwables are indeed
  objects, a property stating that THROWABLE is a subset of OBJECT is
  included.

\item Overloading is not allowed in B and occurs frequently in Java
  Card. To model overloaded methods in B an extension to overloaded
  method names was included.
  
  \end{itemize}

A small piece of specification with some of the characteristics described above is presented in Listing \ref{lis:object}. It presents two \texttt{java.lang} classes: \texttt{Object} and \texttt{Throwable}.  \texttt{Object} is a superclass to  all API classes, with a single method  \texttt{equals} that checks if an object (from which a reference is received as argument) is the same as the current one. \texttt{Throwable} extends \texttt{Object}, but does not define any other method nor redefines \texttt{equals}. The inheritance hierarchy is partially simulated in B by the corresponding set inclusion. These abstract sets are then used to refer to the corresponding class as a type as can be seen in Listing \ref{lis:class-types}.

\lstset{language=B, caption={Basic API Definitions},label=lis:object}
\begin{lstlisting}
MACHINE Object
SEES  javaLangClasses 
OPERATIONS
 	result <-- equals(obj) =
	   PRE obj : OBJECT  /* declared in javaLangClasses */
	   THEN result :: {TRUE, FALSE}

MACHINE Throwable  /* extends java.lang.Object */
SEES
    Object,  javaLangClasses 

MACHINE javaLangClasses
SETS  OBJECT   
CONSTANTS  THROWABLE , ...			
PROPERTIES  THROWABLE <: OBJECT & ...
\end{lstlisting}

\lstset{language=B, caption={Using classes as types},label=lis:class-types}
\begin{lstlisting}
op(anObject,otherObject) = 
	PRE	
		anObject : OBJECT & otherObject : THROWABLE
...
\end{lstlisting}

\paragraph{Discussions on the model}
As previously stated, we chose to model exception raising conditions
as operation pre-conditions in the B models. For instance, if the Java
Card specification states that a method should throw an exception in
case a parameter array is empty, the pre-condition of the
corresponding B operation will require that this parameter is not
empty. The B method then requires that every call to that operation
satisfies the operation's pre-condition. As a consequence, code that
is formally generated using the B method and the Java Card API
specification should never raise this specific exception, as it is
statically proved that all calls to this operation are made with
non-empty parameter arrays. Not all situations leading to exceptional
conditions are modeled, however, as some of them depend on the Java
Card Runtime Environment (JCRE) and its state, which has not yet been
modeled, and some require a more detailed specification of the
contents of some data and other internal behavior. In these cases, the
exception raising conditions are only left as comments to the B
specification, and can either be used as additional documentation or be
considered in future work.

One subtle issue to be dealt with both by the user of the API
specification and the tools designed to work with it, is the use of
overloaded methods in an application development. When overloaded
operations are used in an application development, the user must
explicitly choose which version (in B) of the overloaded operation is to be
used. Then, verifications will be carried out considering this
specific version of the operation. When code is generated, either the
code generator will remove the name extension automatically, if
designed for it, or the user will have to edit the generated code
manually. In any case, it is important that the actual method called
in the Java Card code is the one with which verifications have been
carried out.  In case of overriding, in particular, it will be either
the user's responsibility to choose the B operation in scope at
this specific point in Java, or an extra verification step will be
included in the code generator to check that the operation used in
B is the one in scope in Java and registers an error in case it is
not.

Finally, the choices related to class derived types and return values
were consequences of our focus on the interfaces of the Java Card API
methods. The declaration of an abstract set for each class allows to
model in B that a parameter of a particular class is expected or is to
be returned by a method.

\section{Using the model in BSmart}\label{sec:using-the-API}

The models of the Java Card API are used in the different phases of the 
BSmart method development. Initially, the application 
abstract specification uses the models of basic Java types, 
since Java Card specific aspects are ideally related only
in subsequent refinements.

The BSmart Full Function refinement introduces the modelling of exceptions, 
as stated in section~\ref{sec:api-spec}. This is performed through  the inclusion
of \emph{ISOException} machine, which receives, in its \emph{throwIt} operation, 
a short value corresponding to the \emph{status} code that must be returned to 
the client when the conditions are not satisfied.  

In the B implementation, the whole API can be referenced. Usually,
besides ISOException (or another exception model), a typical Java Card
development imports the \emph{Apdu} and \emph{Util} modules. The first
defines operations to start the process of receiving (from host) and
sending (to host) information through the \emph{apdu buffer}.  
The \emph{Util} component contains useful
operations to get and put data in the buffer. When
translating to \emph{Java Card} the operation calls are translated
to the corresponding \emph{Java Card} method.

As a case study on the use of this API on the formal development of Java Card applications, part of the electronic passport specification\footnote{Available at http://www.icao.int.} is being modeled and developed in BSmart, showing that it is feasible to have a Java Card-like B refinement  such as the one presented in Listing \ref{lis:addimplementation}.

\section{Conclusions and future work}\label{sec:conc}

The B model described in this paper has as intent to be of use to Java Card application developers, either as additional (formal) documentation to the official one, or, better, as an imported library to be used in the formal development of applications with the B method. In section \ref{sec:api-spec} some characteristics and limitations of the work have been presented. Current work on using the API model to formally develop Java Card applications with B shows promising results. 

Among the limitations of this work, some may be dealt with by adapted tools and some will actually require some special attention from the developer, even with tool support, such as method overloading and overriding . These are consequence of B not being object oriented and not providing exception raising and handling mechanisms. Some work on this last item can be seen on \cite{BR2003}, but it has not been implemented.

With the current level of abstraction of the model and the fact that the Java Card Runtime Environment (JCRE) has not been modeled, different conditions which may lead to exception raising are not yet modeled. Extending the model to include them would make developed applications more reliable, as more static verification could be carried
out. Continuation of this work then will enlarge the scope of the modeling to cope statically with a larger set of situations.

\bibliographystyle{plain}
\bibliography{bib}

\end{document}
